COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.TURN OFF "α"
.cb A NATURAL REPRESENTATION

	Here is a systematic way of representing recursively defined
functions by non-recursive sentences of first order logic.  Suppose
the function is given by

!!d1:	%2f = Y(F)%1

in Scottish.  We define

!!d2:	%2 x εε w ≡ ∃w1.(w1 subexp w ∧ x = qaa w1)%1,

and

!!d3:	%2α(w,x) = qif qn assoc(x,w) qthen %AW%2 qelse qd assoc(x,w)%1.

We then define

!!d4:	%2∀w.[table(w,F) ≡ ∀x.[x εε w ≡ α(w,x) = F(λz.α(w,z))(x)]]%1

from which follows

!!d5:	%2∀x y.[y = f(x) ≡ ∃w.[table(w,F) ∧ y = α(w,x)]]%1.

	The functions ε, εε and α are all representable using %2subexp%1.
Sentences ({eq d4}) and ({eq d5}) are not first order in ⊗F, but for
any fixed ⊗F they become first order sentences.  Consider the
rather complicated recursive definition

!!d7:	%2f x ← qif p1 x qthen g1 x qelse qif p2(x,f h1 x) qthen g2 x
qelse g3(x,f g4(x,f g5 x))%1.

({eq d4}) and ({eq d5}) then give

!!d8:	%2∀x y.[y = f x ≡ ∃w.[y = α(w,x) ∧ ∀x.[x εε w ≡
.nofill
α(w,x) = qif p1 x qthen g1 x qelse qif p2(x,α(w,h1 x)) qthen g2 x qelse g3(x,α(w,g4(x,α(w,g5 x))))]]]%1.
.fill
%1
	⊗w, which we will call a %2pair-list%1 of ⊗f,
is a list of (argument.value) pairs for the function ⊗f, and
the second line of ({eq d8}) is obtained by replacing ⊗f(z) by ⊗α(w,z) 
everywhere it occurs in the recursive definition ({eq d7}).  We could
make the notation even more parallel by the syntactic sugar of writing
⊗f' instead of ⊗w and writing %2f'%8<%2z%8>%1 in place of ⊗α(w,x). 
This might well be justified since ⊗w can be regarded as a kind of
finite approximation of the graph of ⊗f that for every (argument.value)
pair it contains, also contains all pairs that come up in its evaluation.
The approximations %AW%1, %2F(%AW%1), %2F(F(%AW%1)), etc. are similar,
but since they include all pairs whose evaluation involves no more than
a certain number of recursions, ordinarily involve an infinite number
of pairs.

	Representing ⊗f by such a sentence characterizing %2pair-lists%1
avoids prescribing an order of evaluation
of terms.  There should be a Church-Rosser type theorem to the effect
that the value of ⊗f(x) is independent of the %2pair-list%1 used.
The use of %2pair-lists%1 rather than computation sequences enabled
us to write the representation of %2Y(F)%1 in terms of %2F%1.  Since
the computation sequence does not depend just on ⊗F we could not write
so simply a representation involving computation sequences.

	However, computation sequences are useful for analyzing time
taken and space used, and here is an approach to formalizing them.
Consider a recursive definition of the form

!!d9:	%2f x ← f1 m x

!!d10:	%2f1 y ← qif p y qthen g y qelse f h y%1.

	Such an ⊗f has a definite computation sequence determined
by ⊗p, ⊗g, and ⊗h, and any recursive function can be put into this
form in a variety of ways.  Each such way determines a computation
sequence.